rules
  adding_to_set_members =
    mems1 -+ mems2 = members from mems1 not in mems2 + members in mems2
    mems -+ mem = mems w/o member with same label as mem + mem
    
  to_structural = T "<:~" T
      R <:~ R 
      { x : S => mems } <:~ { x : S => mems }
      { x => mems } <:~  { x : { x => mems } => mems }
      T1 & T2 <:~ { x : S1 & S2 => mems1 -+ mems2 } 
        if  T1 <:~ { x : S1 => mems1 }
            T2 <:~ { x : S2 => mems2 }
      T # L <:~ R
        if  T <:~ {x => mems}
            mems contains `type L : _ = S`
            x \notin FV(S)
            S <:~ R
      (new T).type <:~ R 
        if  T <:~ R
        
  lookupT = T "has" m "under" x ":" T
    T has m under x : S
      if  T <:~ {x : S => mems}
          mems contains m
          
  eval = 
    (new T).l  ==>  [x -> new T]p  
      if  T has `val l: U = p` under x : _
      
    (new T) <{val l = p}  ==>  new ( T <{val l = p} )
      if  T has `val l: Un[_]` under _ : _
      
    (new T) <{type L = U}  ==>  new ( T <{type L = U} )
      if  T has `type L : Un[_]` under _ : _
      
    new T ==> new (T & {_ => val l: p.type = p}) 
      if  T has `val l: U = t` under x : S
          [x -> new T]t ==> p 
          
    C[t] ==> C[p] 
      if  t ==> p
      
    C[t] = t | t1 <{val l = C[t]} | C[t] <{val l = p} | C[t].l 
    
  of = G "|-" t ":" T 
    G |- new T : T
      if  
          G |- T ~~< {x: S => mems}
          G |- {x: S => mems} : Concrete({x: S => mems})  
          T is not a singleton type 
    G |- p.l : [x -> p]U 
      if  G |- p : {x => val l : U} 
    G |- t.l : U/*'*/ 
      if  G |- t : {x => val l : U} 
          x \notin FV(U/*'*/) 
    G |- t <{ val l = u }   :  T <{val l = u}
      if  G |- t : T
          T has `val l : Un[U]` under x : S 
          G, x: S |- u : U
          x \notin FV(u)
    G |- t <{ type L = U }   :  T <{type L = U}
      if  G |- t : T
          T has `type L : Un[K]` under x : S 
          G, x: S |- U : K
          x \notin FV(U)
    G |- p : p.type
      if  G |- p : T
          T is not a singleton type  
    G |- t : S      
      if  G |- t : T
          G |- T <: S
          
  pathConversion = G "|-" p ~~> p
    G |- p1.l ~~> [x -> p1]p2
      if  G |- p1 : {x => val l : _ = p2}
      
  pathEquality = G "|-" p =~= p
  
  typeConversion = G "|-" T ~~> T
    G |- {x => type L : _ = S}#L ~~> S
    G |- {x : S1 => mems1} & {x : S2 => mems2} ~~> {x : S2 => (mems1 -+ mems2}
      if  G |- S2 <: S1
          mems2 forall{m2 => (mems1 has m2.label) implies 
                                  G |- m2 <: mems1(m2.label) }
    G |- T#L ~~> S#L
      if  G |- T ~~> S
    G |- T <{_} ~~> S <{_}
      if  G |- T ~~> S
    G |- T1 & T2  ~~> S1 & S2
      if  G |- T1 ~~> S1
          G |- T2 ~~> S2
    G |- p.type ~~> q.type
      if G |- p =~= q
    G |- Un[T] ~~> Un[S]
      if  G |- T ~~> S
    G |- p.type#L ~~> [x -> p]S 
      if  G |- p.type <: {x : _ => type L : K = S}  
          K not of shape Nominal(_)
    G |- T#L ~~> S 
      if  G |- T <: {x : _ => type L : K = S} 
          K not of shape Nominal(_)
          x \notin FV(K, S)  
          
  typeEquality = G "|-" T =~= T
  
  typeExpansion = G "|-" T ~~< T
    G |- T ~~< S
      if  G |- T ~~> S
    G |- p.type#L ~~< [x -> p]S 
      if  G |- p.type <: {x : _ => type L : Nominal(_) = S} 
    G |- T#L ~~< S 
      if  G |- T <: {x : _ => type L : Nominal(R) = S}
          x \notin FV(R, S)  
    G |- p.type ~~< T
      if  G |- p : T
      
  subtypingIgnoringDeferred = G "|-" T "<[]:" T
  
  subtyping = G "|-" T "<:" T
    G |- T <: T
    G |- S <: U
      if  G |- S <: T
          G |- T <: U
    G |- T <: Any
      if  G |- T : K 
    G |- Nothing <: T 
      if  G |- T : K 
    G |- Un[S] <: Un[T] 
      if  G |- T <: S
    G |- S <: T
      if  G |- S =~= T
    G |- {x : S => mems} <: {x : S2 => mems2}
      if  G |- S <: S2
          forall m1 in mems, 
            (mems2 has m2 with same label as m1 && 
             G, x : S |- m1 <: m2) || not (m1 deferred).
    G |- T1 & T2 <: T1
    G |- T1 & T2 <: T2
    G |- T <: T1 & T2
      if G |- T <: T1
         G |- T <: T2
    G |- T <: S
      if  G |- T : In(_, S) 
    G |- p.type <: T 
      if  G |- p : T 
        
  memsub = G "|-" m "<:" m
    G |- val l : T (= _)? <: val l : T' (= _)? 
      if G |- T <: T'
    G |- type L : K (= _)?  <:  type L : K'
      if  G |- K <: K'
    G |- type L : K = _   <:  type L : K = _ 
      
  WFmem = G "|-" m "WF"
    G |- val l : T = t WF 
      if  G |- t : T
    G |- type L : Nominal(R) = T  WF 
      if  G |- T : Struct(R) 
    G |- type L : K = T  WF 
      if  G |- T : K
    G |- val l : T  WF  
    G |- type L : K WF  
      
  kinding = G "|-" T ":" K
    G |- {x: S => mems} : Struct({ x : S => mems }) 
      if  mems forall {m => G, x : S |- m WF }
          G |- T <[]: S
          mems no_duplicates
    G |- T1 & T2 : Struct({x : S2 => (mems1 -+ mems2})
      if  G |- T1 : Struct({x : S1 => mems1})
          G |- T2 : Struct({x : S2 => mems2})
          G |- S2 <: S1
          mems2 forall{m2 => (mems1 has m2.label) implies 
                                  G |- m2 <: mems1(m2.label) }
    G |- T : Concrete({x: S => mems})
      if  G |- T : Struct({x: S => mems}) 
          mems forall {m => m deferred XOR m concrete } 
    G |- p.type : Concrete({x: S => mems}) 
      if  G |- p : T
          G |- T : Struct({x: S => mems})
    G |- p.type#L : [x -> p]K 
      if  G |- T : Concrete({x => type L : K})
    G |- T#L : K 
      if  G |- T : Concrete({x => type L : K})
          x \notin FV(K)
    G |- T <{ val l = u } : Struct({x : S => mems -+ `val l : U = u`}) 
      if  G |- T : Struct({x: S => mems}) 
          mems contains `val l : Un[U]`
          G, x: S |- u : U
    G |- T <{ type L = U } : Struct({x : S => mems -+ `type L : K = U`}) 
      if  G |- T : Struct({x: S => mems}) 
          mems contains `type L : Un[K]`
          G, x: S |- U : K
    G |- T : K2 
      if  G |- T : K1
          G |- K1 <: K2
    G |- Any : Struct({x =>})
    G |- Nothing : Struct({x =>})
    G |- Un[T] : K
      if  G |- T : K
      
  subkinding = G "|-" K "<:" K
    G |- Un[K1] <: Un[K2] 
      if  G |- K2 <: K1
    G |- Nominal(R) <: Struct(R)
    G |- Concrete(R) <: Struct(R)
    G |- Struct(R) <: In(S, T) 
      if  G |- S <: R
          G |- R <: T
    G |- Concrete(R1) <: Concrete(R2) 
      if  G |- R1 <: R2 
    G |- Struct(R1) <: Struct(R2) 
      if  G |- R1 <: R2 
    G |- In(T1, T2) <: In(S1, S2) 
      if  G |- T2 <: S2
          G |- S1 <: T1
          
  kind and context formation = G "|-" K
